nLab initial algebra of an endofunctor

Redirected from "Lambek's theorem".
Contents

Context

Algebra

Induction

Contents

Definition

An initial algebra for an endofunctor FF on a category CC is an initial object in the category of algebras of FF. These play a role in particular as the categorical semantics for inductive types.

Properties

Relation to algebras over a monad

The concept of an algebra of an endofunctor is arguably somewhat odd, a more natural concept being that of an algebra over a monad. However, the former can often be reduced to the latter.

Proposition

If 𝒞\mathcal{C} is a complete category, then the category of algebras of an endofunctor F:𝒞𝒞F : \mathcal{C} \to \mathcal{C} is equivalent to the category of algebras over a monad of the free monad on FF, if the latter exists.

The proof is fairly straightforward, see for instance (Maciej) or at free monad.

The existence of free monads, on the other hand, can be a tricky question. One general technique is the transfinite construction of free algebras.

Lambek’s theorem

Theorem

If FF has an initial algebra α:F(X)X\alpha: F(X) \to X, then XX is isomorphic to F(X)F(X) via α\alpha.

Remark

In this sense, XX is a fixed point of FF. Being initial, XX is the smallest fixed point of FF in that there is a map from XX to any other fixed point (indeed, any other algebra), and this map is an injection if CC is Set.

Remark

The dual concept is terminal coalgebra, which is the largest fixed point of FF.

Proof

Given an initial algebra structure α:F(X)X\alpha: F(X) \to X, define an algebra structure on F(X)F(X) to be F(α):F(F(X))F(X)F(\alpha): F(F(X)) \to F(X). By initiality, there exists an FF-algebra map i:XF(X)i: X \to F(X), so that

F(X) F(i) F(F(X)) α F(α) X i F(X)\array{ F(X) & \overset{F(i)}{\to} & F(F(X)) \\ \alpha \downarrow & & \downarrow F(\alpha) \\ X & \underset{i}{\to} & F(X) }

commutes. Now it is trivial, in fact tautological that α\alpha is itself an FF-algebra map F(X)XF(X) \to X. Thus αi=1 X\alpha \circ i = 1_X, since both sides of the equation are FF-algebra maps XXX \to X and XX is initial. As a result, F(α)F(i)=1 F(X)F(\alpha) \circ F(i) = 1_{F(X)}, so that iα=1 F(X)i \circ \alpha = 1_{F(X)} according to the commutative square. Hence α\alpha is an isomorphism, with inverse ii.

Adámek’s theorem

In many cases, initial algebras can be constructed in a recursive/iterative fashion using Adámek's fixed point theorem.

Semantics for inductive types

Initial algebras of endofunctors provide categorical semantics for extensional inductive types. The generalization to weak initial algebras captures the notion in intensional type theory and homotopy type theory.

Examples

Natural numbers

The archetypical example of an initial algebra is the set of natural numbers natural numbers object.

Proposition

Let 𝒯\mathcal{T} be topos and let F:𝒯𝒯F : \mathcal{T} \to \mathcal{T} the functor given by

F:X*X F : X \mapsto * \coprod X

(i.e. the functor underlying the “maybe monad”). Then an initial algebra over FF is precisely a natural number object \mathbb{N} in 𝒯\mathcal{T}.

Proof

By definition, an FF-algebra is an object XX equipped with a morphism

(0,s):*XX, (0,s) : * \coprod X \to X \,,

hence equivalently with a point 0:*X0 : * \to X and an endomorphism s:XXs : X \to X. Initiality means that for any other FF-algebra (0 Y,s Y):*YY(0_Y, s_Y) : * \coprod Y \to Y, there is a unique morphism f:XYf : X \to Y such that the diagram

* 0 X s X f f * 0 Y s Y \array{ * &\stackrel{0}{\to}& X &\stackrel{s}{\to}& X \\ \downarrow && \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{f}} \\ * &\stackrel{0}{\to}& Y &\stackrel{s}{\to}& Y }

commutes. This is the very definition of natural number object X=X = \mathbb{N}.

Bi-pointed sets

Another example of an initial algebra is the bi-pointed set 2\mathbf{2}.

Proposition

Let 𝒯\mathcal{T} be topos and let F:𝒯𝒯F : \mathcal{T} \to \mathcal{T} the functor given by

F:X** F : X \mapsto * \coprod *

Then an initial algebra over FF is precisely a bi-pointed object 2\mathbf{2} in 𝒯\mathcal{T}.

More examples

Theorem applies (in particular) to any functor F:SetSetF: Set \to Set which is a colimit of finitely representable functors hom(n,):XX nhom(n, -): X \mapsto X^n, as in the following examples.

Example

Let AA be a set, and let F:SetSetF: Set \to Set be the functor F(X)=1+A×XF(X) = 1 + A \times X. Then the initial FF-algebra is A *A^*, the free monoid on AA. The FF-algebra structure is

(e,m|):1+A×A *A *(e, m| ): 1 + A \times A^* \to A^*

where e:1A *e: 1 \to A^* is the identity and m|:A×A *A *m|: A \times A^* \to A^* is the restriction of the monoid multiplication along the evident inclusion i×1:A×A *A *×A *i \times 1: A \times A^* \to A^* \times A^*.

This “fixed point” of FF can be thought of as the result of the (slightly nonsensical) calculation

1+A×X=XX=11A=1+A+A 2+=A *1 + A \times X = X \Rightarrow X = \frac1{1 - A} = 1 + A + A^2 + \ldots = A^*

which can be made rigorous by interpreting the initial equality as defining the solution XX by recursion, and applying the theorem above.

Example

Let F:SetSetF: Set \to Set be the functor F(X)=1+X 2F(X) = 1 + X^2. Then the initial FF-algebra is the set TT of isomorphism classes of finite (planar, rooted) binary trees. The FF-algebra structure is

(r,j):1+T 2T(r, j): 1 + T^2 \to T

where r:1Tr: 1 \to T names the tree consisting of just a root vertex, and j:T 2Tj: T^2 \to T creates a tree ttt \vee t' from two trees tt, tt' by joining their roots to a new root, so that the root of tt becomes the left child and the root of tt' the right child of the new root.

The recursive equation

T=1+T 2T = 1 + T^2

would seem to imply that the structure TT behaves something like a structural “sixth root of unity”, and indeed the structural isomorphism TF(T)T \cong F(T) allows one to exhibit an isomorphism

T=T 7T = T^7

constructively, as famously explored by Andreas Blass in the paper “Seven trees in one”.

Example

Let F:SetSetF: Set \to Set be the functor F(X)=X *F(X) = X^* (the free monoid from an earlier example). Then the initial FF-algebra is the set of isomorphism classes of finite planar rooted trees (not necessarily binary as in the previous example).

Example

Let CC be the coslice category Ab\mathbb{Z} \downarrow Ab, and let F:CCF: C \to C be the functor which pushes out along the multiplication-by-pp map p:p \cdot -: \mathbb{Z} \to \mathbb{Z}. Then the initial FF-algebra is the Pruefer group [p 1]/\mathbb{Z}[p^{-1}]/\mathbb{Z}. See the discussion at the n-Category Café, starting here.

Example

Let BanBan be the category of complex Banach spaces and maps of norm bounded above by 11, and let F:BanBanF: \mathbb{C} \downarrow Ban \to \mathbb{C} \downarrow Ban be the squaring functor XX×XX \mapsto X \times X. Then the initial FF-algebra is L 1([0,1])L^1([0, 1]) (with respect to the usual Lebesgue measure). This result is due to Tom Leinster; see this MathOverflow discussion.

Example

A list of notable endofunctors, and their initial algebras/terminal coalgebras.

Nonexistent (co)algebras are labelled with ‘/’, and unknown ones with ‘?’.

Base categoryEndofunctorInitial AlgebraFinal CoalgebraNote, reference
SetConst AAAAAA
SetXXX \mapsto X\varnothing11
SetX1+XX \mapsto 1 + X\mathbb{N}Conatural numbers \mathbb{N}^\inftyextended natural number
SetXA+XX \mapsto A + XA×A \times \mathbb{N}A×+1A \times \mathbb{N} + 1, ie conatural numbers “terminated” (when they aren’t \infty) with AApartial map classifier
SetXX+XX \mapsto X + X or X2×XX \mapsto 2 \times X\emptyset2 2^\mathbb{N} (i.e. one definition of Stream 22)
SetXA×XX \mapsto A \times X\emptysetA A^\mathbb{N} (i.e. one definition of Stream AA)sequence, writer monad, stream
SetXX×XX \mapsto X \times X or X[2,X]X \mapsto [2, X][2,]\emptyset \simeq [2, \emptyset]1 (the unique infinite unlabelled binary tree)
SetX[A,X]X \mapsto [A, X][A,][A, \emptyset]1reader monad
SetX1+A×XX \mapsto 1 + A \times XList AAanother definition of Stream AA; i.e. potentially infinite List AAlist, stream
SetX1+A×X 2X \mapsto 1 + A \times X^2Finite binary tree with AA-labelled nodesPotentially infinite binary tree with AA-labelled nodestree
SetXB+A×X nX \mapsto B + A \times X^nFinite nn-ary tree with AA-labelled nodes and BB-labelled leavesPotentially infinite nn-ary tree with AA-labelled nodes with and BB-labelled leaves
SetXB+A×List(X)X \mapsto B + A \times \text{List}(X)Finite tree with AA-labelled nodes and BB-labelled leavesPotentially infinite tree with AA-labelled nodes with and BB-labelled leavesThe number of subtrees is not fixed to a particular nn, it could be any number
SetXO×[I,X]X \mapsto O \times [I, X]O×[I,]O \times [I, \emptyset]Potentially infinite Moore machine
SetX[I,O×X]X \mapsto [I, O \times X][I,][I, \emptyset]Potentially infinite Mealy machine
SetX𝒫(X)X \mapsto \mathcal{P}(X)//
SetX𝒫 fin(X)X \mapsto \mathcal{P}_{\text{fin}}(X)Finite rooted forestsPotentially infinite finitely-branching rooted forests
Setpolynomial endofunctorW-typeM-type
Bipointed SetsXXXX \mapsto X \vee Xdyadic rational numbers in the interval [0,1][0,1]The closed interval [0,1][0,1] \subseteq \mathbb{R}coalgebra of the real interval
linearly ordered setsXωXX \mapsto \omega \cdot X, where ωX\omega \cdot X is the cartesian product of the natural numbers with the underlying set of XX, equipped with the lexicographic order.\emptysetThe non-negative real numbers 0\mathbb{R}_{\geq 0}real number
Archimedean ordered fieldsXXX \mapsto X the identity functorThe rational numbers \mathbb{Q}The real numbers \mathbb{R}
Archimedean ordered fieldsX𝒟(X)X \mapsto \mathcal{D}(X) where 𝒟(X)\mathcal{D}(X) is the Archimedean ordered field of two-sided Dedekind cuts of XXThe real numbers \mathbb{R}The real numbers \mathbb{R}
Archimedean ordered fieldsX𝒞(X)X \mapsto \mathcal{C}(X) where 𝒞(X)\mathcal{C}(X) is the quotient of Cauchy sequences in the Archimedean ordered field XXThe HoTT book real numbers H\mathbb{R}_HThe Dedekind real numbers \mathbb{R}These are the same objects in the presence of excluded middle or countable choice.
Any categoryThe constant functor XAX \mapsto A given object AAAAAA
Any categoryThe identity functor XXX \mapsto Xinitial objectterminal object
Any extensive categoryX1+XX \mapsto 1 + X given terminal object 11 and coproduct ++natural numbers object?
Any closed abelian categoryXI(AX)X \mapsto I \sqcup (A \otimes X) given tensor unit II, tensor product \otimes, coproduct \sqcup, and object AAtensor algebra of AAcofree coalgebra over AAtensor algebra, cofree coalgebra
\infty -GrpdXΣXX \mapsto \Sigma Xsphere spectrum 𝕊\mathbb{S}?suspension

References

General

A textbook account of the basic theory is in Chapter 10 of

The relation to free monads is discussed in

Original references on initial algebras include

  • Věra Pohlová. “On sums in generalized algebraic categories.” Czechoslovak Mathematical Journal 23.2 (1973): 235-251. http://eudml.org/doc/12718.

  • Jiří Adámek, Free algebras and automata realizations in the language of categories, Commentationes Mathematicae Universitatis Carolinae 15.4 (1974): 589-602.

  • Jiří Adámek, Věra Trnková, Automata and algebras in categories Vol. 37. Springer Science & Business Media, 1990.

Categorical semantics of 𝒲\mathcal{W}-types

The observation that the categorical semantics of well-founded inductive types ( 𝒲 \mathcal{W} -types) is given by initial algebras over polynomial endofunctors on the type system:

Further discussion:

Generalization to inductive families (dependent 𝒲\mathcal{W}-types):

Generalization to homotopy-initial algebras as categorical semantics for 𝒲 \mathcal{W} -types in homotopy type theory:

Towards combining generalization to dependent and homotopical W-types:

Last revised on July 10, 2024 at 00:05:42. See the history of this page for a list of all contributions to it.